【python】sympy的logic文档搬运

The logic module for SymPy allows to form and manipulate logic expressions using symbolic and Boolean values.

You can build Boolean expressions with the standard python operators & (And), | (Or), ~ (Not):

You can also form implications with >> and y Implies(x, y) x 0).as_set() Interval.open(0, oo) And(-2 < x, x < 2).as_set() Interval.open(-2, 2) Or(x < -2, 2 < x).as_set() Union(Interval.open(-oo, -2), Interval.open(2, oo))

equals(other)[source]

Returns True if the given formulas have the same truth table. For two formulas to be equal they must have the same literals.

EXAMPLES

class sympy.logic.boolalg.BooleanTrue[source]

SymPy version of True, a singleton that can be accessed via S.true.

This is the SymPy version of True, for use in the logic module. The primary advantage of using true instead of True is that shorthand Boolean operations like ~ and >> will work as expected on this class, whereas with True they act bitwise on 1. Functions in the logic module will return this class when they evaluate to true.

NOTES

There is liable to be some confusion as to when True should be used and when S.true should be used in various contexts throughout SymPy. An important thing to remember is that sympify(True) returns S.true. This means that for the most part, you can just use True and it will automatically be converted to S.true when necessary, similar to how you can generally use 1 instead of S.One.

The rule of thumb is:

“If the boolean in question can be replaced by an arbitrary symbolic Boolean, like Or(x, y) or x > 1, use S.true. Otherwise, use True”

In other words, use S.true only on those contexts where the boolean is being used as a symbolic representation of truth. For example, if the object ends up in the .args of any expression, then it must necessarily be S.true instead of True, as elements of .args must be Basic. On the other hand, == is not a symbolic operation in SymPy, since it always returns True or False, and does so in terms of structural equality rather than mathematical, so it should return True. The assumptions system should use True and False. Aside from not satisfying the above rule of thumb, the assumptions system uses a three-valued logic (True, False, None), whereas S.true and S.false represent a two-valued logic. When in doubt, use True.

“S.true == True is True.”

While “S.true is True” is False, “S.true == True” is True, so if there is any doubt over whether a function or expression will return S.true or True, just use == instead of is to do the comparison, and it will work in either case. Finally, for boolean flags, it’s better to just use if x instead of if x is True. To quote PEP 8:

Do not compare boolean values to True or False using ==.

Yes: if greeting:

No: if greeting == True:

Worse: if greeting is True:

EXAMPLES

Python operators give a boolean result for true but a bitwise result for True

Python operators give a boolean result for true but a bitwise result for True

See also

sympy.logic.boolalg.BooleanFalse

as_set()[source]

Rewrite logic operators and relationals in terms of real sets.

EXAMPLES

class sympy.logic.boolalg.BooleanFalse[source]

SymPy version of False, a singleton that can be accessed via S.false.

This is the SymPy version of False, for use in the logic module. The primary advantage of using false instead of False is that shorthand Boolean operations like ~ and >> will work as expected on this class, whereas with False they act bitwise on 0. Functions in the logic module will return this class when they evaluate to false.

NOTES

See the notes section in sympy.logic.boolalg.BooleanTrue

EXAMPLES

Python operators give a boolean result for false but a bitwise result for False

See also

sympy.logic.boolalg.BooleanTrue

as_set()[source]

Rewrite logic operators and relationals in terms of real sets.

EXAMPLES

class sympy.logic.boolalg.And(*args)[source]

Logical AND function.

It evaluates its arguments in order, returning false immediately when an argument is false and true if they are all true.

EXAMPLES

NOTES

The & operator is provided as a convenience, but note that its use here is different from its normal use in Python, which is bitwise and. Hence, And(a, b) and a & b will produce different results if a and b are integers.

class sympy.logic.boolalg.Or(*args)[source]

Logical OR function

It evaluates its arguments in order, returning true immediately when an argument is true, and false if they are all false.

EXAMPLES

NOTES

The | operator is provided as a convenience, but note that its use here is different from its normal use in Python, which is bitwise or. Hence, Or(a, b) and a | b will return different things if a and b are integers.

class sympy.logic.boolalg.Not(arg)[source]

Logical Not function (negation)

Returns true if the statement is false or False. Returns false if the statement is true or True.

EXAMPLES

NOTES

The ~ operator is provided as a convenience, but note that its use here is different from its normal use in Python, which is bitwise not. In particular, ~a and Not(a) will be different if a is an integer. Furthermore, since bools in Python subclass from int, ~True is the same as ~1 which is -2, which has a boolean value of True. To avoid this issue, use the SymPy boolean types true and false.

class sympy.logic.boolalg.Xor(*args)[source]

Logical XOR (exclusive OR) function.

Returns True if an odd number of the arguments are True and the rest are False.

Returns False if an even number of the arguments are True and the rest are False.

EXAMPLES

NOTES

The ^ operator is provided as a convenience, but note that its use here is different from its normal use in Python, which is bitwise xor. In particular, a ^ b and Xor(a, b) will be different if a and b are integers.

class sympy.logic.boolalg.Nand(*args)[source]

Logical NAND function.

It evaluates its arguments in order, giving True immediately if any of them are False, and False if they are all True.

Returns True if any of the arguments are False Returns False if all arguments are True

EXAMPLES

class sympy.logic.boolalg.Nor(*args)[source]

Logical NOR function.

It evaluates its arguments in order, giving False immediately if any of them are True, and True if they are all False.

Returns False if any argument is True Returns True if all arguments are False

EXAMPLES

class sympy.logic.boolalg.Xnor(*args)[source]

Logical XNOR function.

Returns False if an odd number of the arguments are True and the rest are False.

Returns True if an even number of the arguments are True and the rest are False.

EXAMPLES

class sympy.logic.boolalg.Implies(*args)[source]

Logical implication.

A implies B is equivalent to if A then B. Mathematically, it is written as \(A \Rightarrow B\) and is equivalent to \(\neg A \vee B\) or ~A | B.

Accepts two Boolean arguments; A and B. Returns False if A is True and B is False Returns True otherwise.

EXAMPLES

class sympy.logic.boolalg.Equivalent(*args)[source]

Equivalence relation.

Equivalent(A, B) is True iff A and B are both True or both False.

Returns True if all of the arguments are logically equivalent. Returns False otherwise.

For two arguments, this is equivalent to Xnor.

EXAMPLES

class sympy.logic.boolalg.ITE(*args)[source]

If-then-else clause.

ITE(A, B, C) evaluates and returns the result of B if A is true else it returns the result of C. All args must be Booleans.

From a logic gate perspective, ITE corresponds to a 2-to-1 multiplexer, where A is the select signal.

EXAMPLES

Trying to use non-Boolean args will generate a TypeError:

class sympy.logic.boolalg.Exclusive(*args)[source]

True if only one or no argument is true.

Exclusive(A, B, C) is equivalent to ~(A & B) & ~(A & C) & ~(B & C).

For two arguments, this is equivalent to Xor.

EXAMPLES

The following functions can be used to handle Algebraic, Conjunctive, Disjunctive, and Negated Normal forms:

sympy.logic.boolalg.to_anf(expr, deep=True)[source]

Converts expr to Algebraic Normal Form (ANF).

ANF is a canonical normal form, which means that two equivalent formulas will convert to the same ANF.

A logical expression is in ANF if it has the form

\[1 \oplus a \oplus b \oplus ab \oplus abc\]

i.e. it can be:

purely true,

purely false,

conjunction of variables,

exclusive disjunction.

The exclusive disjunction can only contain true, variables or conjunction of variables. No negations are permitted.

If deep is False, arguments of the boolean expression are considered variables, i.e. only the top-level expression is converted to ANF.

EXAMPLES

sympy.logic.boolalg.to_cnf(expr, simplify=False, force=False)[source]

Convert a propositional logical sentence expr to conjunctive normal form: ((A | ~B | ...) & (B | C | ...) & ...). If simplify is True, expr is evaluated to its simplest CNF form using the Quine-McCluskey algorithm; this may take a long time. If there are more than 8 variables the force flag must be set to True to simplify (default is False).

EXAMPLES

sympy.logic.boolalg.to_dnf(expr, simplify=False, force=False)[source]

Convert a propositional logical sentence expr to disjunctive normal form: ((A & ~B & ...) | (B & C & ...) | ...). If simplify is True, expr is evaluated to its simplest DNF form using the Quine-McCluskey algorithm; this may take a long time. If there are more than 8 variables, the force flag must be set to True to simplify (default is False).

EXAMPLES

sympy.logic.boolalg.to_nnf(expr, simplify=True)[source]

Converts expr to Negation Normal Form (NNF).

A logical expression is in NNF if it contains only And, Or and Not, and Not is applied only to literals. If simplify is True, the result contains no redundant clauses.

EXAMPLES

sympy.logic.boolalg.is_anf(expr)[source]

Checks if expr is in Algebraic Normal Form (ANF).

A logical expression is in ANF if it has the form

\[1 \oplus a \oplus b \oplus ab \oplus abc\]

i.e. it is purely true, purely false, conjunction of variables or exclusive disjunction. The exclusive disjunction can only contain true, variables or conjunction of variables. No negations are permitted.

EXAMPLES

sympy.logic.boolalg.is_cnf(expr)[source]

Test whether or not an expression is in conjunctive normal form.

EXAMPLES

sympy.logic.boolalg.is_dnf(expr)[source]

Test whether or not an expression is in disjunctive normal form.

EXAMPLES

sympy.logic.boolalg.is_nnf(expr, simplified=True)[source]

Checks if expr is in Negation Normal Form (NNF).

A logical expression is in NNF if it contains only And, Or and Not, and Not is applied only to literals. If simplified is True, checks if result contains no redundant clauses.

EXAMPLES

sympy.logic.boolalg.gateinputcount(expr)[source]

Return the total number of inputs for the logic gates realizing the Boolean expression.

Returns:

int

NOTE

Not all Boolean functions count as gate here, only those that are considered to be standard gates. These are: And, Or, Xor, Not, and ITE (multiplexer). Nand, Nor, and Xnor will be evaluated to Not(And()) etc.

EXAMPLES

Note that Nand is automatically evaluated to Not(And()) so

Although this can be avoided by using evaluate=False

Also note that a comparison will count as a Boolean variable:

As will a symbol: >>> gateinputcount(x) 0

sympy.logic.boolalg.simplify_logic(expr, form=None, deep=True, force=False, dontcare=None)[source]

This function simplifies a boolean function to its simplified version in SOP or POS form. The return type is an Or or And object in SymPy.

Parameters:

expr : Boolean

form : string ('cnf' or 'dnf') or None (default).

deep : bool (default True)

force : bool (default False)

dontcare : Boolean

EXAMPLES

REFERENCES

[R574]

https://en.wikipedia.org/wiki/Don%27t-care_term

SymPy’s simplify() function can also be used to simplify logic expressions to their simplest forms.

sympy.logic.boolalg.bool_map(bool1, bool2)[source]

Return the simplified version of bool1, and the mapping of variables that makes the two expressions bool1 and bool2 represent the same logical behaviour for some correspondence between the variables of each. If more than one mappings of this sort exist, one of them is returned.

For example, And(x, y) is logically equivalent to And(a, b) for the mapping {x: a, y: b} or {x: b, y: a}. If no such mapping exists, return False.

EXAMPLES

The results are not necessarily unique, but they are canonical. Here, (w, z) could be (a, d) or (d, a):

The following functions can be used to manipulate Boolean expressions:

sympy.logic.boolalg.distribute_and_over_or(expr)[source]

Given a sentence expr consisting of conjunctions and disjunctions of literals, return an equivalent sentence in CNF.

EXAMPLES

sympy.logic.boolalg.distribute_or_over_and(expr)[source]

Given a sentence expr consisting of conjunctions and disjunctions of literals, return an equivalent sentence in DNF.

Note that the output is NOT simplified.

EXAMPLES

sympy.logic.boolalg.distribute_xor_over_and(expr)[source]

Given a sentence expr consisting of conjunction and exclusive disjunctions of literals, return an equivalent exclusive disjunction.

Note that the output is NOT simplified.

EXAMPLES

sympy.logic.boolalg.eliminate_implications(expr)[source]

Change Implies and Equivalent into And, Or, and Not. That is, return an expression that is equivalent to expr, but has only &, |, and ~ as logical operators.

EXAMPLES

It is possible to create a truth table for a Boolean function with

sympy.logic.boolalg.truth_table(expr, variables, input=True)[source]

Return a generator of all possible configurations of the input variables, and the result of the boolean expression for those values.

Parameters:

expr : Boolean expression

variables : list of variables

input : bool (default True)

EXAMPLES

If input is False, truth_table returns only a list of truth values. In this case, the corresponding input values of variables can be deduced from the index of a given output.

For mapping between integer representations of truth table positions, lists of zeros and ones and symbols, the following functions can be used:

sympy.logic.boolalg.integer_to_term(n, bits=None, str=False)[source]

Return a list of length bits corresponding to the binary value of n with small bits to the right (last). If bits is omitted, the length will be the number required to represent n. If the bits are desired in reversed order, use the [::-1] slice of the returned list.

If a sequence of all bits-length lists starting from [0, 0,..., 0] through [1, 1, ..., 1] are desired, pass a non-integer for bits, e.g. 'all'.

If the bit string is desired pass str=True.

EXAMPLES

If all lists corresponding to 0 to 2**n - 1, pass a non-integer for bits:

If a bit string is desired of a given length, use str=True:

sympy.logic.boolalg.term_to_integer(term)[source]

Return an integer corresponding to the base-2 digits given by term.

Parameters:

term : a string or list of ones and zeros

EXAMPLES

sympy.logic.boolalg.bool_maxterm(k, variables)[source]

Return the k-th maxterm.

Each maxterm is assigned an index based on the opposite conventional binary encoding used for minterms. The maxterm convention assigns the value 0 to the direct form and 1 to the complemented form.

Parameters:

k : int or list of 1’s and 0’s (complementation pattern)

variables : list of variables

EXAMPLES

REFERENCES

[R575]

https://en.wikipedia.org/wiki/Canonical_normal_form#Indexing_maxterms

sympy.logic.boolalg.bool_minterm(k, variables)[source]

Return the k-th minterm.

Minterms are numbered by a binary encoding of the complementation pattern of the variables. This convention assigns the value 1 to the direct form and 0 to the complemented form.

Parameters:

k : int or list of 1’s and 0’s (complementation pattern)

variables : list of variables

EXAMPLES

REFERENCES

[R576]

https://en.wikipedia.org/wiki/Canonical_normal_form#Indexing_minterms

sympy.logic.boolalg.bool_monomial(k, variables)[source]

Return the k-th monomial.

Monomials are numbered by a binary encoding of the presence and absences of the variables. This convention assigns the value 1 to the presence of variable and 0 to the absence of variable.

Each boolean function can be uniquely represented by a Zhegalkin Polynomial (Algebraic Normal Form). The Zhegalkin Polynomial of the boolean function with \(n\) variables can contain up to \(2^n\) monomials. We can enumerate all the monomials. Each monomial is fully specified by the presence or absence of each variable.

For example, boolean function with four variables (a, b, c, d) can contain up to \(2^4 = 16\) monomials. The 13-th monomial is the product a & b & d, because 13 in binary is 1, 1, 0, 1.

Parameters:

k : int or list of 1’s and 0’s

variables : list of variables

EXAMPLES

sympy.logic.boolalg.anf_coeffs(truthvalues)[source]

Convert a list of truth values of some boolean expression to the list of coefficients of the polynomial mod 2 (exclusive disjunction) representing the boolean expression in ANF (i.e., the “Zhegalkin polynomial”).

There are \(2^n\) possible Zhegalkin monomials in \(n\) variables, since each monomial is fully specified by the presence or absence of each variable.

We can enumerate all the monomials. For example, boolean function with four variables (a, b, c, d) can contain up to \(2^4 = 16\) monomials. The 13-th monomial is the product a & b & d, because 13 in binary is 1, 1, 0, 1.

A given monomial’s presence or absence in a polynomial corresponds to that monomial’s coefficient being 1 or 0 respectively.

EXAMPLES

sympy.logic.boolalg.to_int_repr(clauses, symbols)[source]

Takes clauses in CNF format and puts them into an integer representation.

EXAMPLES

This module implements some inference routines in propositional logic.

The function satisfiable will test that a given Boolean expression is satisfiable, that is, you can assign values to the variables to make the sentence True.

For example, the expression x & ~x is not satisfiable, since there are no values for x that make this sentence True. On the other hand, (x | y) & (x | ~y) & (~x | y) is satisfiable with both x and y being True.

As you see, when a sentence is satisfiable, it returns a model that makes that sentence True. If it is not satisfiable it will return False.

sympy.logic.inference.satisfiable(expr, algorithm=None, all_models=False, minimal=False)[source]

Check satisfiability of a propositional sentence. Returns a model when it succeeds. Returns {true: true} for trivially true expressions.

On setting all_models to True, if given expr is satisfiable then returns a generator of models. However, if expr is unsatisfiable then returns a generator containing the single element False.

EXAMPLES